; COMMAND-LINE: --finite-model-find
(set-logic ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun $$rtu (Real) $$unsorted)
(declare-fun $$utr ($$unsorted) Real)
(assert (let ((_let_1 (to_real 1))) (= _let_1 ($$utr ($$rtu _let_1)))))
(declare-fun tptp.include ($$unsorted) Bool)
(assert (tptp.include ($$rtu (to_real 1))))
(assert (= (/ 8 5) ($$utr ($$rtu (/ 8 5)))))
(declare-fun tptp.e ($$unsorted $$unsorted) Bool)
(assert (forall ((E $$unsorted)) (tptp.e E ($$rtu (/ 8 5)))))
(assert (= 3000.0 ($$utr ($$rtu 3000.0))))
(assert (forall ((A $$unsorted) (E $$unsorted)) (not (tptp.e A ($$rtu 3000.0)))))
(assert (= (/ 13 5) ($$utr ($$rtu (/ 13 5)))))
(assert (not (forall ((E $$unsorted)) (tptp.e E ($$rtu (/ 13 5))))))
(set-info :filename tptp_parser9)
(check-sat-assuming ( true ))
